PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 14:08:44 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 majority.prism majority.props --property change_state -const T=2100
Parsing model file "majority.prism"...
Type: CTMC
Modules: D_def Y_def Z_def CC_def XX_def EE_def
Variables: D Y Z CC XX EE
Parsing properties file "majority.props"...
1 property:
(1) "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]
Property constants: T=2100
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 44 iterations in 0.04 seconds (average 0.000932, setup 0.00)
Time for model construction: 44.95 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Rate matrix: 9569 nodes (85 terminal), 1961600 minterms, vars: 43r/43c
Computing probabilities...
Engine: Sparse
Number of non-absorbing states: 189000 of 192000 (98.4%)
Building sparse matrix... [n=192000, nnz=1933200, compact] [7.6 MB]
Creating vector for diagonals... [1.5 MB]
Allocating iteration vectors... [3 x 1.5 MB]
TOTAL: [13.4 MB]
Uniformisation: q.t = 3.287227 x 2100.000000 = 6903.175850
Fox-Glynn: left = 6319, right = 7610
Starting iterations...
Iteration 832 (of 7610): max relative diff=0.011047, 5.00 sec so far
Iteration 1661 (of 7610): max relative diff=0.002316, 10.01 sec so far
Iteration 2490 (of 7610): max relative diff=0.000969, 15.01 sec so far
Iteration 3320 (of 7610): max relative diff=0.000549, 20.01 sec so far
Iteration 4149 (of 7610): max relative diff=0.000376, 25.02 sec so far
Iteration 4978 (of 7610): max relative diff=0.000284, 30.02 sec so far
Iteration 5808 (of 7610): max relative diff=0.000228, 35.02 sec so far
Iteration 6628 (of 7610): max relative diff=0.000191, 40.03 sec so far
Iteration 7428 (of 7610): max relative diff=0.000164, 45.04 sec so far
Iterative method: 7610 iterations in 51.12 seconds (average 0.006068, setup 4.95)
Value in the initial state: 0.05429919316250449
Time for model checking: 51.027 seconds.
Result: 0.05429919316250449 (value in the initial state)
Overall running time: 96.568 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.